『Type-Driven Development with Idris』

https://gyazo.com/c13b2ff9b8f8a5a4a80953baf4491b59

PART 1: INTRODUCTION

1. OVERVIEW ►

2. GETTING STARTED WITH IDRIS ►

PART 2: CORE IDRIS

3. INTERACTIVE DEVELOPMENT WITH TYPES ►

4. USER DEFINED DATA TYPES ►

5. INTERACTIVE PROGRAMS: INPUT AND OUTPUT PROCESSING ▸

6. PROGRAMMING WITH FIRST CLASS TYPES ‣

7. INTERFACES: USING CONSTRAINED GENERIC TYPES ►

8. EQUALITY: EXPRESSING RELATIONSHIPS BETWEEN DATA ►

9. PREDICATES: EXPRESSING ASSUMPTIONS AND CONTRACTS IN TYPES ►

10. VIEWS: EXTENDING PATTERN MATCHING ►

PART 3: IDRIS AND THE REAL WORLD

11. STREAMS AND PROCESSES: WORKING WITH INFINITE DATA ►

12. WRITING PROGRAMS WITH STATE ▸

13. STATE MACHINES: VERIFYING PROTOCOLS IN TYPES ‣

14. DEPENDENT STATE MACHINES: HANDLING FEEDBACK AND ERRORS ►

15. TYPE-SAFE CONCURRENT PROGRAMMING ►

APPENDIXES

APPENDIX A: INSTALLING IDRIS AND EDITOR MODES ►

APPENDIX B: INTERACTIVE EDITING COMMANDS

APPENDIX C: REPL COMMANDS

APPENDIX D: THE PACKAGING SYSTEM